2021-04-11 03:39:27 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=360ms, Wt=365ms. NTI: Rt=8ms, Wt=6ms at most 91 inferences for useful informations.
% NTI summary: 0 cases unresolved, 1 predicate has been ignored: [integer/1]

exp(A,B)terminates_if b(A).
    % optimal. loops found: [exp(['('|_],x)]. NTI took    0ms,87i,87i WARNING: ignored predicates: [integer/1]
pdt(A,B)terminates_if b(A).
    % optimal. loops found: [pdt([_,_,_|_],x)]. NTI took    0ms,80i,80i WARNING: ignored predicates: [integer/1]
pri(A,B)terminates_if b(A).
    % optimal. loops found: [pri(['('|_],x)]. NTI took    0ms,82i,82i WARNING: ignored predicates: [integer/1]
rdp(A,B)terminates_if b(A).
    % optimal. loops found: [rdp([_,_|_],x)]. NTI took    4ms,73i,73i WARNING: ignored predicates: [integer/1]
rds(A,B)terminates_if b(A).
    % optimal. loops found: [rds([_,_|_],x)]. NTI took    0ms,78i,78i WARNING: ignored predicates: [integer/1]
som(A,B)terminates_if b(A).
    % optimal. loops found: [som([_,_,_|_],x)]. NTI took    0ms,91i,91i WARNING: ignored predicates: [integer/1]

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 12 proofs the 6 inferred conditions:

exp(b, f).
    % ==> termination proof established
exp(f, b).
    % ==> no proof found
pdt(b, f).
    % ==> termination proof established
pdt(f, b).
    % ==> no proof found
pri(b, f).
    % ==> termination proof established
pri(f, b).
    % ==> no proof found
rdp(b, f).
    % ==> termination proof established
rdp(f, b).
    % ==> no proof found
rds(b, f).
    % ==> termination proof established
rds(f, b).
    % ==> no proof found
som(b, f).
    % ==> termination proof established
som(f, b).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program:

som(U,V):-pdt(U,W),rds(W,V).
pdt(U,V):-pri(U,W),rdp(W,V).
pri([N|U],U):-integer(N).
pri(['('|U],V):-exp(U,[')'|V]).
rds(U,U).
rds([Op|U],V):-pdt(U,W),rds(W,V).
rdp(U,U).
rdp([Op|U],V):-pri(U,W),rdp(W,V).
exp(U,V):-som(U,V).